1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import analysis.calculus.mean_value
src         └──────────────────────────┘
  8  import tactic.monotonicity
src         └─────────────────┘
  9  
 10  /-!
 11  # Extending differentiability to the boundary
 12  
 13  We investigate how differentiable functions inside a set extend to differentiable functions
 14  on the boundary. For this, it suffices that the function and its derivative admit limits there.
 15  A general version of this statement is given in `has_fderiv_at_boundary_of_tendsto_fderiv`.
 16  
 17  One-dimensional versions, in which one wants to obtain differentiability at the left endpoint or
 18  the right endpoint of an interval, are given in
 19  `has_deriv_at_interval_left_endpoint_of_tendsto_deriv` and
 20  `has_deriv_at_interval_right_endpoint_of_tendsto_deriv`. These versions are formulated in terms
 21  of the one-dimensional derivative `deriv ℝ f`.
 22  -/
 23  
 24  set_option class.instance_max_depth 40
doc             └──────────────────────┘
 25  
 26  variables {E : Type*} [normed_group E] [normed_space ℝ E]
 27            {F : Type*} [normed_group F] [normed_space ℝ F]
 28  
 29  open filter set metric continuous_linear_map
 30  open_locale topological_space
 31  local attribute [mono] prod_mono
id                          └───────┘
src                         └───────┘
typ                         └───────┘
doc                   └──┘
 32  
 33  /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
 34  derivative converges to `0` at a point on the boundary, then `f` is differentiable there with
 35  derivative `0`. This is an auxiliary statement to prove the same result for any value of the
 36  derivative, in `has_fderiv_at_boundary_of_tendsto_fderiv`. -/
 37  theorem has_fderiv_at_boundary_of_tendsto_fderiv_aux {f : E → F} {s : set E} {x : E}
 38    (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
 39    (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
 40    (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 0)) :
 41    has_fderiv_within_at f (0 : E →L[ℝ] F) (closure s) x :=
 42  begin
 43    classical,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
 44    -- one can assume without loss of generality that `x` belongs to the closure of `s`, as the
 45    -- statement is empty otherwise
 46    by_cases hx : x ∉ closure s,
src    └───────┘  └─┘         
typ    └───────┘  └─┘         
doc    └───────┘  └─┘         
txt    └───────┘  └─┘         
par    └───────┘  └─┘         
pid              └─┘         
 47    { rw ← closure_closure at hx, exact has_fderiv_within_at_of_not_mem_closure hx },
src      └───┘               └────┘  └────┘                                         
typ      └───┘               └────┘  └────┘                                         
doc      └───┘               └────┘  └────┘                                         
txt      └───┘               └────┘  └────┘                                         
par      └───┘               └────┘  └────┘                                         
pid        └─┘               └────┘                                                
 48    push_neg at hx,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid            └────┘
 49    /- One needs to show that `∥f y - f x∥ ≤ ε ∥y - x∥` for `y` close to `x` in `closure s`, where
 50    `ε` is an arbitrary positive constant. By continuity of the functions, it suffices to prove this
 51    for nearby points inside `s`. In a neighborhood of `x`, the derivative of `f` is arbitrarily small
 52    by assumption. The mean value inequality ensures that `f` is `ε`-Lipschitz there, concluding the
 53    proof. -/
 54    assume ε ε_pos,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
 55    obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ∥fderiv ℝ f y∥ < ε,
id                                             └──┘         └────┘        
src    └──────────────────────┘ └────┘ └───┘  └──┘    └────┘    
typ    └──────────────────────┘ └────┘ └───┘ └──┘   └────┘   
doc    └──────────────────────┘ └────┘  └───┘            └────┘     
txt    └──────────────────────┘ └────┘  └───┘                       
par    └──────────────────────┘ └────┘  └───┘                       
pid          └────────────────┘ └────┘  └───┘                       
st                                   └───────────────────────────────────────────┘
 56      by simpa [dist_zero_right] using tendsto_nhds_within_nhds.1 h ε ε_pos,
id                 └─────────────┘        └──────────────────────┘     └───┘
src         └─────┘└─────────────┘└──────┘└──────────────────────┘└─┘  
typ         └─────┘└─────────────┘└──────┘└──────────────────────┘└─┘└───┘
doc         └─────┘               └──────┘                        └─┘  
txt         └─────┘               └──────┘                        └─┘  
par         └─────┘               └──────┘                        └─┘  
pid                             └────┘                        └─┘  
st                                                                            └─
 57    set B := ball x δ,
id              └──┘  
src    └───────┘└──┘ 
typ    └───────┘└──┘
doc    └───────┘└──┘ 
txt    └───────┘     
par    └───────┘     
pid       └┘     
st   ──────────────────┘└─
 58    suffices : ∀ y ∈ B ∩ (closure s), ∥f y - f x∥ ≤ ε * ∥y - x∥,
id                         └─────┘                      
src    └─────────┘ └───┘  └─────┘            
typ    └─────────┘ └───┘ └─────┘         
doc    └─────────┘ └───┘   └─────┘               
txt    └─────────┘ └───┘                         
par    └─────────┘ └───┘                         
pid    └───────┘└┘ └───┘                         
st   ────────────────────────────────────────────────────────────┘└─
 59      from mem_nhds_within_iff.2 ⟨δ, δ_pos, λy hy, by simpa using this y hy⟩,
id            └─────────────────┘      └───┘                        └──┘  └┘
src      └───┘└─────────────────┘└─┘  └┘     └┘ └────┘  └──────────┘       
typ      └───┘└─────────────────┘└─┘ └┘└───┘└┘ └────┘  └──────────┘└──┘└┘
doc      └───┘                   └─┘  └┘     └┘ └────┘  └──────────┘       
txt      └───┘                   └─┘  └┘     └┘ └────┘  └──────────┘       
par      └───┘                   └─┘  └┘     └┘ └────┘  └──────────┘       
pid      └───┘                   └─┘  └┘     └┘ └────┘  └───────────┘       
st   ──────────────────────────────────────────────────┘└────────────────────┘└─
 60    suffices : ∀ p : E × E, p ∈ closure ((B ∩ s).prod (B ∩ s)) → ∥f p.2 - f p.1∥ ≤ ε * ∥p.2 - p.1∥,
id                              └─────┘                                         
src    └─────────┘ └───┘     └─────┘     └─────┘    └─┘    └─┘   └┘      └─┘  └┘
typ    └─────────┘ └───┘   └─────┘     └─────┘  └─┘    └─┘  └┘     └─┘  └┘
doc    └─────────┘ └───┘      └─────┘     └─────┘    └─┘    └─┘   └┘      └─┘  └┘
txt    └─────────┘ └───┘                  └─────┘    └─┘    └─┘   └┘      └─┘  └┘
par    └─────────┘ └───┘                  └─────┘    └─┘    └─┘   └┘      └─┘  └┘
pid    └───────┘└┘ └───┘                  └─────┘    └─┘    └─┘   └┘      └─┘  └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
 61    { rw closure_prod_eq at this,
id          └─────────────┘
src      └─┘└─────────────┘└──────┘
typ      └─┘└─────────────┘└──────┘
doc      └─┘               └──────┘
txt      └─┘               └──────┘
par      └─┘               └──────┘
pid                       └──────┘
st   ───┘└────────────────────────┘└─
 62      intros y y_in,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid            └─────┘
st   ────────────────┘└─
 63      apply this ⟨x, y⟩,
id             └──┘    
src      └────┘      └┘ 
typ      └────┘└──┘ └┘
doc      └────┘      └┘ 
txt      └────┘      └┘ 
par      └────┘      └┘ 
pid                 └┘ 
st   ────────────────────┘└─
 64      have : B ∩ closure s ⊆ closure (B ∩ s), from closure_inter_open is_open_ball,
id                             └─────┘             └────────────────┘ └──────────┘
src      └─────┘          └─────┘      └───┘└────────────────┘└──────────┘
typ      └─────┘          └─────┘    └───┘└────────────────┘└──────────┘
doc      └─────┘           └─────┘      └───┘                  
txt      └─────┘                        └───┘                  
par      └─────┘                        └───┘                  
pid      └───┘└┘                        └───┘                  
st   ─────────────────────────────────────────┘└────────────────────────────────────┘└─
 65      exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩ },
id                    └───────────┘ └───┘  └┘   └──┘ └──┘
src      └────┘      └───────────┘     └┘  └─┘        └┘
typ      └────┘      └───────────┘└───┘└┘└┘└─┘└──┘└──┘└┘
doc      └────┘                        └┘  └─┘        └┘
txt      └────┘                        └┘  └─┘        └┘
par      └────┘                        └┘  └─┘        └┘
pid                                   └┘  └─┘        
st   ─────────────────────────────────────────────────────┘└┘
 66    have key : ∀ p : E × E, p ∈ (B ∩ s).prod (B ∩ s) → ∥f p.2 - f p.1∥ ≤ ε * ∥p.2 - p.1∥,
id                                                                     
src    └─────────┘ └───┘          └─────┘    └┘    └─┘   └┘      └─┘  └┘
typ    └─────────┘ └───┘        └─────┘  └┘    └─┘  └┘     └─┘  └┘
doc    └─────────┘ └───┘          └─────┘    └┘    └─┘   └┘      └─┘  └┘
txt    └─────────┘ └───┘          └─────┘    └┘    └─┘   └┘      └─┘  └┘
par    └─────────┘ └───┘          └─────┘    └┘    └─┘   └┘      └─┘  └┘
pid    └──────┘└─┘ └───┘          └─────┘    └┘    └─┘   └┘      └─┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
 67    { rintros ⟨u, v⟩ ⟨u_in, v_in⟩,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid             └──────────────────┘
st   ───┘└─────────────────────────┘└─
 68      have conv : convex (B ∩ s) := (convex_ball _ _).inter s_conv,
id                   └────┘           └─────────┘            └────┘
src      └──────────┘└────┘    └───┘ └─────────┘└──────────┘
typ      └──────────┘└────┘  └───┘ └─────────┘└──────────┘└────┘
doc      └──────────┘└────┘    └───┘            └──────────┘
txt      └──────────┘          └───┘            └──────────┘
par      └──────────┘          └───┘            └──────────┘
pid      └───────┘└─┘          └──┘            └──────────┘
st   ───────────────────────────────────────────────────────────────┘└─
 69      have diff : differentiable_on ℝ f (B ∩ s) := f_diff.mono (inter_subset_right _ _),
id                   └───────────────┘             └─────────┘  └────────────────┘
src      └──────────┘└───────────────┘      └───┘└─────────┘ └────────────────┘└───┘
typ      └──────────┘└───────────────┘   └───┘└─────────┘ └────────────────┘└───┘
doc      └──────────┘└───────────────┘      └───┘                              └───┘
txt      └──────────┘                       └───┘                              └───┘
par      └──────────┘                       └───┘                              └───┘
pid      └───────┘└─┘                       └──┘                              └───┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
 70      refine conv.norm_image_sub_le_of_norm_deriv_le diff (λz z_in, _) u_in v_in,
id              └─────────────────────────────────────┘ └──┘              └──┘ └──┘
src      └─────┘└─────────────────────────────────────┘      └─────────┘    
typ      └─────┘└─────────────────────────────────────┘└──┘  └─────────┘└──┘└──┘
doc      └─────┘└─────────────────────────────────────┘      └─────────┘    
txt      └─────┘                                             └─────────┘    
par      └─────┘                                             └─────────┘    
pid                                                         └─────────┘    
st   ─────────────────────────────────────────────────────────────────────────────┘└─
 71      convert le_of_lt (hδ _ z_in.2 z_in.1),
id               └──────┘  └┘          └──┘
src      └──────┘└──────┘   └─┘    └─┘    └─┘
typ      └──────┘└──────┘ └┘└─┘    └─┘└──┘└─┘
doc      └──────┘           └─┘    └─┘    └─┘
txt      └──────┘           └─┘    └─┘    └─┘
par      └──────┘           └─┘    └─┘    └─┘
pid                        └─┘    └─┘    └─┘
st   ────────────────────────────────────────┘└─
 72      have op : is_open (B ∩ s) := is_open_inter is_open_ball s_open,
id                 └─────┘          └───────────┘ └──────────┘ └────┘
src      └────────┘└─────┘    └───┘└───────────┘└──────────┘
typ      └────────┘└─────┘  └───┘└───────────┘└──────────┘└────┘
doc      └────────┘└─────┘    └───┘                         
txt      └────────┘           └───┘                         
par      └────────┘           └───┘                         
pid      └─────┘└─┘           └──┘                         
st   ─────────────────────────────────────────────────────────────────┘└─
 73      rw differentiable_at.fderiv_within _ (op.unique_diff_on z z_in),
id          └─────────────────────────────┘    └───────────────┘  └──┘
src      └─┘└─────────────────────────────┘└─┘ └───────────────┘     
typ      └─┘└─────────────────────────────┘└─┘ └───────────────┘└──┘
doc      └─┘                               └─┘                       
txt      └─┘                               └─┘                       
par      └─┘                               └─┘                       
pid                                       └─┘                       
st   ──────────────────────────────────────────────────────────────────┘└─
 74      exact (diff z z_in).differentiable_at (mem_nhds_sets op z_in) },
id              └──┘                           └───────────┘ └┘ └──┘
src      └────┘          └──────────────────┘ └───────────┘      └┘
typ      └────┘ └──┘    └──────────────────┘ └───────────┘└┘└──┘└┘
doc      └────┘          └──────────────────┘                    └┘
txt      └────┘          └──────────────────┘                    └┘
par      └────┘          └──────────────────┘                    └┘
pid                     └──────────────────┘                    
st   ─────────────────────────────────────────────────────────────────┘└┘
 75    rintros ⟨u, v⟩ uv_in,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid           └───────────┘
st   ─────────────────────┘└─
 76    refine continuous_within_at.closure_le uv_in _ _ key,
id            └─────────────────────────────┘ └───┘     └─┘
src    └─────┘└─────────────────────────────┘     └───┘
typ    └─────┘└─────────────────────────────┘└───┘└───┘└─┘
doc    └─────┘                                    └───┘
txt    └─────┘                                    └───┘
par    └─────┘                                    └───┘
pid                                              └───┘
st   ─────────────────────────────────────────────────────┘└─
 77    all_goals { -- common start for both continuity proofs
src    └──────────────────────────────────────────────────────
typ    └──────────────────────────────────────────────────────
doc    └──────────────────────────────────────────────────────
txt    └──────────────────────────────────────────────────────
par    └──────────────────────────────────────────────────────
pid             └─────────────────────────────────────────────
st   ────────────┘└───────────────────────────────────────────
 78      have : (B ∩ s).prod (B ∩ s) ⊆ s.prod s, by mono ; exact inter_subset_right _ _,
id                                    └────┘                   └────────────────┘
src  ───┘└─────┘    └─────┘    └┘ └────┘ └───┘└───┘└┘└────┘└────────────────┘└──┘└─
typ  ───┘└─────┘    └─────┘   └┘ └────┘└───┘└───┘└┘└────┘└────────────────┘└──┘└─
doc  ───┘└─────┘    └─────┘    └┘ └────┘ └───┘└───┘└┘└────┘                  └──┘└─
txt  ───┘└─────┘    └─────┘    └┘        └───┘└───┘└┘└────┘                  └──┘└─
par  ───┘└─────┘    └─────┘    └┘        └───┘└───┘└┘└────┘                  └──┘└─
pid  ──────────┘    └─────┘    └┘        └────────────────┘                  └─────
st   ─────────────────────────────────────────┘                                        └─
 79      obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s,
id                                               └─────┘ 
src  ───┘└────────────────────┘             └─────┘ └─
typ  ───┘└────────────────────┘           └─────┘└─
doc  ───┘└────────────────────┘             └─────┘ └─
txt  ───┘└────────────────────┘                     └─
par  ───┘└────────────────────┘                     └─
pid  ─────────────────────────┘                     └─
st   ──────────────────────────────────────────────────────┘
 80        by simpa [closure_prod_eq] using closure_mono this uv_in,
id                   └─────────────┘        └──────────┘ └──┘ └───┘
src  ────────┘└─────┘└─────────────┘└──────┘└──────────┘         └─
typ  ────────┘└─────┘└─────────────┘└──────┘└──────────┘└──┘└───┘└─
doc  ────────┘└─────┘               └──────┘                     └─
txt  ────────┘└─────┘               └──────┘                     └─
par  ────────┘└─────┘               └──────┘                     └─
pid  ───────────────┘               └──────┘                     └─
st                                                                 └─
 81      apply continuous_within_at.mono _ this,
id             └───────────────────────┘   └──┘
src  ───┘└────┘└───────────────────────┘└─┘    └─
typ  ───┘└────┘└───────────────────────┘└─┘└──┘└─
doc  ───┘└────┘                         └─┘    └─
txt  ───┘└────┘                         └─┘    └─
par  ───┘└────┘                         └─┘    └─
pid  ─────────┘                         └─┘    └─
st   ─────────────────────────────────────────┘└─
 82      simp only [continuous_within_at, nhds_prod_eq] },
id                  └──────────────────┘  └──────────┘
src  ───┘└─────────┘└──────────────────┘└┘└──────────┘└┘
typ  ───┘└─────────┘└──────────────────┘└┘└──────────┘└┘
doc  ───┘└─────────┘└──────────────────┘└┘            └┘
txt  ───┘└─────────┘                    └┘            └┘
par  ───┘└─────────┘                    └┘            └┘
pid  ──────────────┘                    └┘            └─┘
st   ──────────────────────────────────────────────────┘└┘
 83    { rw nhds_within_prod_eq,
id          └─────────────────┘
src      └─┘└─────────────────┘
typ      └─┘└─────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└────────────────────┘└─
 84      exact tendsto.comp continuous_norm.continuous_at
id                          └───────────────────────────┘
src      └────┘            └───────────────────────────┘
typ      └────┘            └───────────────────────────┘
doc      └────┘                                         
txt      └────┘                                         
par      └────┘                                         
pid                                                    
st   ─────────────────────────────────────────────────────
 85        ((tendsto.comp (f_cont v v_in) tendsto_snd).sub $ tendsto.comp (f_cont u u_in) tendsto_fst) },
id                                 └──┘  └─────────┘        └──────────┘  └────┘  └──┘  └─────────┘
src  ─────┘                          └┘└─────────┘└────┘ └──────────┘            └┘└─────────┘└┘
typ  ─────┘                     └──┘└┘└─────────┘└────┘ └──────────┘ └────┘└──┘└┘└─────────┘└┘
doc  ─────┘                          └┘           └────┘                         └┘           └┘
txt  ─────┘                          └┘           └────┘                         └┘           └┘
par  ─────┘                          └┘           └────┘                         └┘           └┘
pid  ─────┘                          └┘           └────┘                         └┘           
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
 86    { apply tendsto_nhds_within_of_tendsto_nhds,
id             └─────────────────────────────────┘
src      └────┘└─────────────────────────────────┘
typ      └────┘└─────────────────────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────────────────────────────┘└─
 87      rw nhds_prod_eq,
id          └──────────┘
src      └─┘└──────────┘
typ      └─┘└──────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────┘└─
 88      exact tendsto_const_nhds.mul
id             └────────────────────┘
src      └────┘└────────────────────┘
typ      └────┘└────────────────────┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ─────────────────────────────────
 89        (tendsto.comp continuous_norm.continuous_at $ tendsto_snd.sub tendsto_fst) },
id          └──────────┘ └───────────────────────────┘   └─────────────┘ └─────────┘
src  ─────┘ └──────────┘└───────────────────────────┘ └─────────────┘└─────────┘└┘
typ  ─────┘ └──────────┘└───────────────────────────┘ └─────────────┘└─────────┘└┘
doc  ─────┘                                                                     └┘
txt  ─────┘                                                                     └┘
par  ─────┘                                                                     └┘
pid  ─────┘                                                                     
st   ────────────────────────────────────────────────────────────────────────────────┘└──
 90  end
st   ──┘
 91  
 92  /-- If a function `f` is differentiable in a convex open set and continuous on its closure, and its
 93  derivative converges to a limit `f'` at a point on the boundary, then `f` is differentiable there
 94  with derivative `f'`. -/
 95  theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : set E} {x : E} {f' : E →L[ℝ] F}
id                                                                   └─┘                 └─┘ 
src                                                                    └─┘                    └─┘
typ                                                                  └─┘                 └─┘ 
doc                                                                                           └─┘ 
 96    (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s)
id               └───────────────┘               └────┘             └─────┘ 
src              └───────────────┘                 └────┘              └─────┘
typ              └───────────────┘               └────┘             └─────┘ 
doc              └───────────────┘                  └────┘              └─────┘
 97    (f_cont : ∀y ∈ closure s, continuous_within_at f s y)
id                   └─────┘   └──────────────────┘   
src                   └─────┘    └──────────────────┘
typ                  └─────┘   └──────────────────┘   
doc                   └─────┘    └──────────────────┘
 98    (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 f')) :
id          └─────┘     └────┘      └─────────┘      └┘
src         └─────┘      └────┘        └─────────┘       
typ         └─────┘     └────┘      └─────────┘      └┘
doc         └─────┘      └────┘         └─────────┘       
 99    has_fderiv_within_at f f' (closure s) x :=
id     └──────────────────┘  └┘  └─────┘   
src    └──────────────────┘       └─────┘
typ    └──────────────────┘  └┘  └─────┘   
doc    └──────────────────┘       └─────┘
100  begin
st   └─────
101    /- We subtract `f'` to define a new function `g` for which `g' = 0`, for which differentiability
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
102    is proved `has_fderiv_at_boundary_of_differentiable_aux`. Then, we just need to glue together the
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
103    pieces, expressing back `f` in terms of `g`. -/
st   ──────────────────────────────────────────────────
104    let g := λy, f y - f' y,
id                      └┘
src    └───────┘ └─┘    
typ    └───────┘ └─┘ └┘
doc    └───────┘ └─┘     
txt    └───────┘ └─┘     
par    └───────┘ └─┘     
pid    └───┘└─┘ └─┘     
st   ────────────────────────┘└─
105    have diff_g : differentiable_on ℝ g s :=
id                   └───────────────┘    
src    └────────────┘└───────────────┘   └───
typ    └────────────┘└───────────────┘ └───
doc    └────────────┘└───────────────┘   └───
txt    └────────────┘                    └───
par    └────────────┘                    └───
pid    └─────────┘└─┘                    └───
st   ───────────────────────────────────────────
106      f_diff.sub (f'.differentiable.comp differentiable_id).differentiable_on,
id       └────────┘  └────────────────────┘ └───────────────┘
src  ───┘└────────┘ └────────────────────┘└───────────────┘└─────────────────┘
typ  ───┘└────────┘ └────────────────────┘└───────────────┘└─────────────────┘
doc  ───┘                                                  └─────────────────┘
txt  ───┘                                                  └─────────────────┘
par  ───┘                                                  └─────────────────┘
pid  ───┘                                                  └────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
107    have cont_g : ∀y ∈ closure s, continuous_within_at g s y :=
id                        └─────┘    └──────────────────┘  
src    └────────────┘ └──┘└─────┘  └──────────────────┘   └───
typ    └────────────┘ └──┘└─────┘  └──────────────────┘ └───
doc    └────────────┘ └──┘└─────┘  └──────────────────┘   └───
txt    └────────────┘ └──┘                                └───
par    └────────────┘ └──┘                                └───
pid    └─────────┘└─┘ └──┘                                └───
st   ──────────────────────────────────────────────────────────────
108      λy hy, tendsto.sub (f_cont y hy) (f'.continuous.comp continuous_id).continuous_within_at,
id              └─────────┘  └────┘        └────────────────┘ └───────────┘
src  ───┘ └────┘└─────────┘          └┘ └────────────────┘└───────────┘└────────────────────┘
typ  ───┘ └────┘└─────────┘ └────┘   └┘ └────────────────┘└───────────┘└────────────────────┘
doc  ───┘ └────┘                     └┘                                └────────────────────┘
txt  ───┘ └────┘                     └┘                                └────────────────────┘
par  ───┘ └────┘                     └┘                                └────────────────────┘
pid  ───┘ └────┘                     └┘                                └───────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
109    have A : ∀y ∈ s, fderiv ℝ f y - f' = fderiv ℝ g y,
id                                   └┘  └────┘   
src    └───────┘ └──┘              └────┘  
typ    └───────┘ └──┘          └┘└────┘ 
doc    └───────┘ └──┘               └────┘  
txt    └───────┘ └──┘                       
par    └───────┘ └──┘                       
pid    └────┘└─┘ └──┘                       
st   ──────────────────────────────────────────────────┘└─
110    { assume y hy,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
111      have : has_fderiv_at f (fderiv ℝ f y) y :=
id              └───────────┘    └────┘       
src      └─────┘└───────────┘  └────┘   └┘ └───
typ      └─────┘└───────────┘  └────┘  └┘└───
doc      └─────┘└───────────┘  └────┘   └┘ └───
txt      └─────┘                        └┘ └───
par      └─────┘                        └┘ └───
pid      └───┘└┘                        └┘ └───
st   ───────────────────────────────────────────────
112        (differentiable_within_at.differentiable_at (f_diff y hy) (mem_nhds_sets s_open hy)).has_fderiv_at,
id          └────────────────────────────────────────┘  └────┘       └───────────┘ └────┘ └┘
src  ─────┘ └────────────────────────────────────────┘          └┘ └───────────┘        └──────────────┘
typ  ─────┘ └────────────────────────────────────────┘ └────┘  └┘ └───────────┘└────┘└┘└──────────────┘
doc  ─────┘                                                     └┘                      └──────────────┘
txt  ─────┘                                                     └┘                      └──────────────┘
par  ─────┘                                                     └┘                      └──────────────┘
pid  ─────┘                                                     └┘                      └─────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
113      have : has_fderiv_at g (fderiv ℝ f y - f') y :=
id              └───────────┘   └────┘        └┘  
src      └─────┘└───────────┘  └────┘      └┘ └───
typ      └─────┘└───────────┘ └────┘   └┘└┘└───
doc      └─────┘└───────────┘  └────┘      └┘ └───
txt      └─────┘                           └┘ └───
par      └─────┘                           └┘ └───
pid      └───┘└┘                           └┘ └───
st   ────────────────────────────────────────────────────
114        this.sub (f'.has_fderiv_at.comp y (has_fderiv_at_id y)),
id         └──────┘  └───────────────────┘    └──────────────┘ 
src  ─────┘└──────┘ └───────────────────┘  └──────────────┘ └┘
typ  ─────┘└──────┘ └───────────────────┘  └──────────────┘└┘
doc  ─────┘         └───────────────────┘                   └┘
txt  ─────┘                                                 └┘
par  ─────┘                                                 └┘
pid  ─────┘                                                 └┘
st   ────────────────────────────────────────────────────────────┘└─
115      exact this.fderiv.symm },
id             └──────────────┘
src      └────┘└──────────────┘
typ      └────┘└──────────────┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ──────────────────────────┘└┘
116    have B : tendsto (λy, fderiv ℝ f y - f') (nhds_within x s) (𝓝 (f' - f')) :=
id              └─────┘      └────┘             └─────────┘            └┘
src    └───────┘└─────┘  └─┘└────┘      └┘ └─────────┘  └┘       └─────
typ    └───────┘└─────┘  └─┘└────┘     └┘ └─────────┘└┘     └┘└─────
doc    └───────┘└─────┘  └─┘└────┘      └┘ └─────────┘  └┘       └─────
txt    └───────┘         └─┘            └┘              └┘        └─────
par    └───────┘         └─┘            └┘              └┘        └─────
pid    └────┘└─┘         └─┘            └┘              └┘        └┘└───
st   ──────────────────────────────────────────────────────────────────────────────
117      h.sub tendsto_const_nhds,
id       └───┘ └────────────────┘
src  ───┘└───┘└────────────────┘
typ  ───┘└───┘└────────────────┘
doc  ───┘     
txt  ───┘     
par  ───┘     
pid  ───┘     
st   ───────────────────────────┘└─
118    have : tendsto (λy, fderiv ℝ g y) (nhds_within x s) (𝓝 0),
id            └─────┘      └────┘        └─────────┘  
src    └─────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └─┘
typ    └─────┘└─────┘  └─┘└────┘  └┘ └─────────┘└┘  └─┘
doc    └─────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └─┘
txt    └─────┘         └─┘         └┘              └┘  └─┘
par    └─────┘         └─┘         └┘              └┘  └─┘
pid    └───┘└┘         └─┘         └┘              └┘  └─┘
st   ──────────────────────────────────────────────────────────┘└─
119    { have : f' - f' = 0, by simp,
id                   └┘
src      └─────┘      └┘     └──┘
typ      └─────┘   └┘ └┘     └──┘
doc      └─────┘      └┘     └──┘
txt      └─────┘      └┘     └──┘
par      └─────┘      └┘     └──┘
pid      └───┘└┘      
st   ───┘└────────────────┘         └─
120      rw this at B,
id          └──┘
src      └─┘    └───┘
typ      └─┘└──┘└───┘
doc      └─┘    └───┘
txt      └─┘    └───┘
par      └─┘    └───┘
pid            └───┘
st   ───────────────┘└─
121      apply tendsto.congr' _ B,
id             └────────────┘   
src      └────┘└────────────┘└─┘
typ      └────┘└────────────┘└─┘
doc      └────┘              └─┘
txt      └────┘              └─┘
par      └────┘              └─┘
pid                         └─┘
st   ───────────────────────────┘└─
122      filter_upwards [self_mem_nhds_within] A },
id                       └──────────────────┘  
src      └──────────────┘└──────────────────┘└┘ 
typ      └──────────────┘└──────────────────┘└┘
doc      └──────────────┘                    └┘ 
txt      └──────────────┘                    └┘ 
par      └──────────────┘                    └┘ 
pid                    └┘                     
st   ───────────────────────────────────────────┘└┘
123    have : has_fderiv_within_at g (0 : E →L[ℝ] F) (closure s) x :=
id            └──────────────────┘        └─┘     └─────┘   
src    └─────┘└──────────────────┘  └──┘ └─┘  └┘ └─────┘ └┘ └───
typ    └─────┘└──────────────────┘ └──┘└─┘ └┘ └─────┘└┘└───
doc    └─────┘└──────────────────┘  └──┘ └─┘  └┘ └─────┘ └┘ └───
txt    └─────┘                      └──┘       └┘         └┘ └───
par    └─────┘                      └──┘       └┘         └┘ └───
pid    └───┘└┘                      └──┘       └┘         └┘ └───
st   ─────────────────────────────────────────────────────────────────
124      has_fderiv_at_boundary_of_tendsto_fderiv_aux diff_g s_conv s_open cont_g this,
id       └──────────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └──┘
src  ───┘└──────────────────────────────────────────┘                        
typ  ───┘└──────────────────────────────────────────┘└────┘└────┘└────┘└────┘└──┘
doc  ───┘└──────────────────────────────────────────┘                        
txt  ───┘                                                                    
par  ───┘                                                                    
pid  ───┘                                                                    
st   ────────────────────────────────────────────────────────────────────────────────┘└─
125    convert this.add f'.has_fderiv_within_at,
id             └──────┘ └─────────────────────┘
src    └──────┘└──────┘└─────────────────────┘
typ    └──────┘└──────┘└─────────────────────┘
doc    └──────┘        
txt    └──────┘        
par    └──────┘        
pid                   
st   ─────────────────────────────────────────┘└─
126    { ext y, simp [g] },
id                    
src      └───┘  └────┘ └┘
typ      └───┘  └────┘└┘
doc      └───┘  └────┘ └┘
txt      └───┘  └────┘ └┘
par      └───┘  └────┘ └┘
pid         └┘       
st   ───┘└───┘└─────────┘└┘
127    { simp }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
128  end
st   ──┘
129  
130  /-- If a function is differentiable on the right of a point `a : ℝ`, continuous at `a`, and
131  its derivative also converges at `a`, then `f` is differentiable on the right at `a`. -/
132  lemma has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
id                                                                   └─┘                         
src                                                                  └─┘                       
typ                                                                  └─┘                         
133    (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
id               └───────────────┘              └──────────────────┘   
src              └───────────────┘                └──────────────────┘
typ              └───────────────┘              └──────────────────┘   
doc              └───────────────┘                 └──────────────────┘
134    (hs : s ∈ nhds_within a (Ioi a))
id             └─────────┘   └─┘ 
src             └─────────┘    └─┘
typ            └─────────┘   └─┘ 
doc              └─────────┘    └─┘
135    (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Ioi a)) (𝓝 e)) :
id               └─────┘     └───┘     └─────────┘   └─┘      
src              └─────┘      └───┘       └─────────┘    └─┘      
typ              └─────┘     └───┘     └─────────┘   └─┘      
doc              └─────┘      └───┘       └─────────┘    └─┘      
136    has_deriv_within_at f e (Ici a) a :=
id     └─────────────────┘    └─┘   
src    └─────────────────┘      └─┘
typ    └─────────────────┘    └─┘   
doc    └─────────────────┘      └─┘
137  begin
st   └─────
138    /- This is a specialization of `has_fderiv_at_boundary_of_tendsto_fderiv`. To be in the setting of
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
139    this theorem, we need to work on an open interval with closure contained in `s ∪ {a}`, that we
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
140    call `t = (a, b)`. Then, we check all the assumptions of this theorem and we apply it. -/
st   ────────────────────────────────────────────────────────────────────────────────────────────
141    obtain ⟨b, ab, sab⟩ : ∃ b ∈ Ioi a, Ioc a b ⊆ s :=
id                                └─┘   └─┘     
src    └────────────────────┘└───┘└─┘ └─┘   └───
typ    └────────────────────┘└───┘└─┘ └─┘ └───
doc    └────────────────────┘ └───┘└─┘  └─┘    └───
txt    └────────────────────┘ └───┘            └───
par    └────────────────────┘ └───┘            └───
pid          └──────────────┘ └───┘            └───
st   ────────────────────────────────────────────────────
142      mem_nhds_within_Ioi_iff_exists_Ioc_subset.1 hs,
id       └───────────────────────────────────────┘   └┘
src  ───┘└───────────────────────────────────────┘└─┘
typ  ───┘└───────────────────────────────────────┘└─┘└┘
doc  ───┘└───────────────────────────────────────┘└─┘
txt  ───┘                                         └─┘
par  ───┘                                         └─┘
pid  ───┘                                         └─┘
st   ─────────────────────────────────────────────────┘└─
143    let t := Ioo a b,
id              └─┘  
src    └───────┘└─┘ 
typ    └───────┘└─┘
doc    └───────┘└─┘ 
txt    └───────┘    
par    └───────┘    
pid    └───┘└─┘    
st   ─────────────────┘└─
144    have ts : t ⊆ s := subset.trans Ioo_subset_Ioc_self sab,
id                      └──────────┘ └─────────────────┘ └─┘
src    └────────┘   └──┘└──────────┘└─────────────────┘
typ    └────────┘ └──┘└──────────┘└─────────────────┘└─┘
doc    └────────┘   └──┘                               
txt    └────────┘   └──┘                               
par    └────────┘   └──┘                               
pid    └─────┘└─┘   └──┘                               
st   ────────────────────────────────────────────────────────┘└─
145    have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
id                   └───────────────┘        └─────────┘ └┘
src    └────────────┘└───────────────┘   └──┘└─────────┘
typ    └────────────┘└───────────────┘ └──┘└─────────┘└┘
doc    └────────────┘└───────────────┘   └──┘           
txt    └────────────┘                    └──┘           
par    └────────────┘                    └──┘           
pid    └─────────┘└─┘                    └──┘           
st   ────────────────────────────────────────────────────────┘└─
146    have t_conv : convex t := convex_Ioo a b,
id                   └────┘     └────────┘  
src    └────────────┘└────┘ └──┘└────────┘ 
typ    └────────────┘└────┘└──┘└────────┘
doc    └────────────┘└────┘ └──┘           
txt    └────────────┘       └──┘           
par    └────────────┘       └──┘           
pid    └─────────┘└─┘       └──┘           
st   ─────────────────────────────────────────┘└─
147    have t_open : is_open t := is_open_Ioo,
id                   └─────┘     └─────────┘
src    └────────────┘└─────┘ └──┘└─────────┘
typ    └────────────┘└─────┘└──┘└─────────┘
doc    └────────────┘└─────┘ └──┘
txt    └────────────┘        └──┘
par    └────────────┘        └──┘
pid    └─────────┘└─┘        └──┘
st   ───────────────────────────────────────┘└─
148    have t_closure : closure t = Icc a b := closure_Ioo ab,
id                      └─────┘   └─┘      └─────────┘ └┘
src    └───────────────┘└─────┘ └─┘  └──┘└─────────┘
typ    └───────────────┘└─────┘└─┘└──┘└─────────┘└┘
doc    └───────────────┘└─────┘  └─┘  └──┘└─────────┘
txt    └───────────────┘              └──┘           
par    └───────────────┘              └──┘           
pid    └────────────┘└─┘              └──┘           
st   ───────────────────────────────────────────────────────┘└─
149    have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
id                        └─────┘    └──────────────────┘  
src    └────────────┘ └──┘└─────┘  └──────────────────┘  
typ    └────────────┘ └──┘└─────┘  └──────────────────┘
doc    └────────────┘ └──┘└─────┘  └──────────────────┘  
txt    └────────────┘ └──┘                               
par    └────────────┘ └──┘                               
pid    └─────────┘└─┘ └──┘                               
st   ─────────────────────────────────────────────────────────┘└─
150    { rw t_closure,
id          └───────┘
src      └─┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└──────────┘└─
151      assume y hy,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
152      by_cases h : y = a,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
153      { rw h, exact f_lim.mono ts },
id                    └────────┘ └┘
src        └─┘   └────┘└────────┘  
typ        └─┘  └────┘└────────┘└┘
doc        └─┘   └────┘            
txt        └─┘   └────┘            
par        └─┘   └────┘            
pid                              
st   ─────┘└──┘└────────────────────┘└┘
154      { have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (ne.symm h), hy.2⟩,
id                       └─┘  └────────────┘       └─────┘    └┘
src        └─────┘   └──┘    └────────────┘  └─┘ └─────┘ └─┘  └─┘
typ        └─────┘ └──┘└─┘ └────────────┘  └─┘ └─────┘└─┘└┘└─┘
doc        └─────┘   └──┘                    └─┘         └─┘  └─┘
txt        └─────┘   └──┘                    └─┘         └─┘  └─┘
par        └─────┘   └──┘                    └─┘         └─┘  └─┘
pid        └───┘└┘   └──┘                    └─┘         └─┘  └─┘
st   ────────────────────────────────────────────────────────────────┘└─
155        exact (f_diff.continuous_on y this).mono ts } },
id                └──────────────────┘  └──┘       └┘
src        └────┘ └──────────────────┘     └─────┘  
typ        └────┘ └──────────────────┘└──┘└─────┘└┘
doc        └────┘                          └─────┘  
txt        └────┘                          └─────┘  
par        └────┘                          └─────┘  
pid                                       └─────┘  
st   ─────────────────────────────────────────────────┘└──┘
156    have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
id                    └─────┘      └────┘        └─────────┘       └────────┘   
src    └─────────────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └────────┘└─┘ └┘
typ    └─────────────┘└─────┘  └─┘└────┘  └┘ └─────────┘└┘  └────────┘└─┘└┘
doc    └─────────────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └────────┘└─┘ └┘
txt    └─────────────┘         └─┘         └┘              └┘             └─┘ └┘
par    └─────────────┘         └─┘         └┘              └┘             └─┘ └┘
pid    └──────────┘└─┘         └─┘         └┘              └┘             └─┘ └┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
157    { simp [deriv_fderiv.symm],
src      └────┘                 
typ      └────┘└───────────────┘
doc      └────┘                 
txt      └────┘                 
par      └────┘                 
pid                           
st   ───┘└──────────────────────┘└─
158      refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
id              └──────────┘ └───────────────────────────────────────────────────────────────┘
src      └─────┘└──────────┘└───────────────────────────────────────────────────────────────┘└┘
typ      └─────┘└──────────┘└───────────────────────────────────────────────────────────────┘└┘
doc      └─────┘            └───────────────────────────────────────────────────────────────┘└┘
txt      └─────┘                                                                             └┘
par      └─────┘                                                                             └┘
pid                                                                                         └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
159      exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' },
id             └─────────────┘  └──────────────┘   └─────────────────┘  └────┘
src      └────┘└─────────────┘ └──────────────┘└─┘└─────────────────┘└┘      
typ      └────┘└─────────────┘ └──────────────┘└─┘└─────────────────┘└┘└────┘
doc      └────┘                                └─┘                   └┘      
txt      └────┘                                └─┘                   └┘      
par      └────┘                                └─┘                   └┘      
pid                                           └─┘                   └┘      
st   ─────────────────────────────────────────────────────────────────────────┘└┘
160    -- now we can apply `has_fderiv_at_boundary_of_differentiable`
st   ─────────────────────────────────────────────────────────────────
161    have : has_deriv_within_at f e (Icc a b) a,
id            └─────────────────┘    └─┘     
src    └─────┘└─────────────────┘   └─┘  └┘
typ    └─────┘└─────────────────┘ └─┘ └┘
doc    └─────┘└─────────────────┘   └─┘  └┘
txt    └─────┘                           └┘
par    └─────┘                           └┘
pid    └───┘└┘                           └┘
st   ───────────────────────────────────────────┘└─
162    { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],
id           └──────────────────────────────────────────┘    └───────┘
src      └──┘└──────────────────────────────────────────┘└──┘         
typ      └──┘└──────────────────────────────────────────┘└──┘└───────┘
doc      └──┘└──────────────────────────────────────────┘└──┘         
txt      └──┘                                            └──┘         
par      └──┘                                            └──┘         
pid        └┘                                            └──┘         
st   ───┘└──────────────────────────────────────────────┘└───────────┘└──
163      exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff' },
id             └──────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └─────┘
src      └────┘└──────────────────────────────────────┘                               
typ      └────┘└──────────────────────────────────────┘└────┘└────┘└────┘└────┘└─────┘
doc      └────┘└──────────────────────────────────────┘                               
txt      └────┘                                                                       
par      └────┘                                                                       
pid                                                                                  
st   ──────────────────────────────────────────────────────────────────────────────────────┘└┘
164    exact this.nhds_within (mem_nhds_within_Ici_iff_exists_Icc_subset.2 ⟨b, ab, subset.refl _⟩)
id           └──────────────┘  └───────────────────────────────────────┘      └┘  └─────────┘
src    └────┘└──────────────┘ └───────────────────────────────────────┘└─┘  └┘  └┘└─────────┘└───┘
typ    └────┘└──────────────┘ └───────────────────────────────────────┘└─┘ └┘└┘└┘└─────────┘└───┘
doc    └────┘                 └───────────────────────────────────────┘└─┘  └┘  └┘           └───┘
txt    └────┘                                                          └─┘  └┘  └┘           └───┘
par    └────┘                                                          └─┘  └┘  └┘           └───┘
pid                                                                   └─┘  └┘  └┘           └──┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘
165  end
st   └─┘
166  
167  /-- If a function is differentiable on the left of a point `a : ℝ`, continuous at `a`, and
168  its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
169  lemma has_fderiv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
id                                                                     └─┘                         
src                                                                    └─┘                       
typ                                                                    └─┘                         
170    (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
id               └───────────────┘              └──────────────────┘   
src              └───────────────┘                └──────────────────┘
typ              └───────────────┘              └──────────────────┘   
doc              └───────────────┘                 └──────────────────┘
171    (hs : s ∈ nhds_within a (Iio a))
id             └─────────┘   └─┘ 
src             └─────────┘    └─┘
typ            └─────────┘   └─┘ 
doc              └─────────┘    └─┘
172    (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Iio a)) (𝓝 e)) :
id               └─────┘     └───┘     └─────────┘   └─┘      
src              └─────┘      └───┘       └─────────┘    └─┘      
typ              └─────┘     └───┘     └─────────┘   └─┘      
doc              └─────┘      └───┘       └─────────┘    └─┘      
173    has_deriv_within_at f e (Iic a) a :=
id     └─────────────────┘    └─┘   
src    └─────────────────┘      └─┘
typ    └─────────────────┘    └─┘   
doc    └─────────────────┘      └─┘
174  begin
st   └─────
175    /- This is a specialization of `has_fderiv_at_boundary_of_differentiable`. To be in the setting of
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
176    this theorem, we need to work on an open interval with closure contained in `s ∪ {a}`, that we
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
177    call `t = (b, a)`. Then, we check all the assumptions of this theorem and we apply it. -/
st   ────────────────────────────────────────────────────────────────────────────────────────────
178    obtain ⟨b, ba, sab⟩ : ∃ b ∈ Iio a, Ico b a ⊆ s :=
id                                └─┘   └─┘     
src    └────────────────────┘└───┘└─┘ └─┘   └───
typ    └────────────────────┘└───┘└─┘ └─┘ └───
doc    └────────────────────┘ └───┘└─┘  └─┘    └───
txt    └────────────────────┘ └───┘            └───
par    └────────────────────┘ └───┘            └───
pid          └──────────────┘ └───┘            └───
st   ────────────────────────────────────────────────────
179      mem_nhds_within_Iio_iff_exists_Ico_subset.1 hs,
id       └───────────────────────────────────────┘   └┘
src  ───┘└───────────────────────────────────────┘└─┘
typ  ───┘└───────────────────────────────────────┘└─┘└┘
doc  ───┘└───────────────────────────────────────┘└─┘
txt  ───┘                                         └─┘
par  ───┘                                         └─┘
pid  ───┘                                         └─┘
st   ─────────────────────────────────────────────────┘└─
180    let t := Ioo b a,
id              └─┘  
src    └───────┘└─┘ 
typ    └───────┘└─┘
doc    └───────┘└─┘ 
txt    └───────┘    
par    └───────┘    
pid    └───┘└─┘    
st   ─────────────────┘└─
181    have ts : t ⊆ s := subset.trans Ioo_subset_Ico_self sab,
id                      └──────────┘ └─────────────────┘ └─┘
src    └────────┘   └──┘└──────────┘└─────────────────┘
typ    └────────┘ └──┘└──────────┘└─────────────────┘└─┘
doc    └────────┘   └──┘                               
txt    └────────┘   └──┘                               
par    └────────┘   └──┘                               
pid    └─────┘└─┘   └──┘                               
st   ────────────────────────────────────────────────────────┘└─
182    have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
id                   └───────────────┘        └─────────┘ └┘
src    └────────────┘└───────────────┘   └──┘└─────────┘
typ    └────────────┘└───────────────┘ └──┘└─────────┘└┘
doc    └────────────┘└───────────────┘   └──┘           
txt    └────────────┘                    └──┘           
par    └────────────┘                    └──┘           
pid    └─────────┘└─┘                    └──┘           
st   ────────────────────────────────────────────────────────┘└─
183    have t_conv : convex t := convex_Ioo b a,
id                   └────┘     └────────┘  
src    └────────────┘└────┘ └──┘└────────┘ 
typ    └────────────┘└────┘└──┘└────────┘
doc    └────────────┘└────┘ └──┘           
txt    └────────────┘       └──┘           
par    └────────────┘       └──┘           
pid    └─────────┘└─┘       └──┘           
st   ─────────────────────────────────────────┘└─
184    have t_open : is_open t := is_open_Ioo,
id                   └─────┘     └─────────┘
src    └────────────┘└─────┘ └──┘└─────────┘
typ    └────────────┘└─────┘└──┘└─────────┘
doc    └────────────┘└─────┘ └──┘
txt    └────────────┘        └──┘
par    └────────────┘        └──┘
pid    └─────────┘└─┘        └──┘
st   ───────────────────────────────────────┘└─
185    have t_closure : closure t = Icc b a := closure_Ioo ba,
id                      └─────┘   └─┘      └─────────┘ └┘
src    └───────────────┘└─────┘ └─┘  └──┘└─────────┘
typ    └───────────────┘└─────┘└─┘└──┘└─────────┘└┘
doc    └───────────────┘└─────┘  └─┘  └──┘└─────────┘
txt    └───────────────┘              └──┘           
par    └───────────────┘              └──┘           
pid    └────────────┘└─┘              └──┘           
st   ───────────────────────────────────────────────────────┘└─
186    have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
id                        └─────┘    └──────────────────┘  
src    └────────────┘ └──┘└─────┘  └──────────────────┘  
typ    └────────────┘ └──┘└─────┘  └──────────────────┘
doc    └────────────┘ └──┘└─────┘  └──────────────────┘  
txt    └────────────┘ └──┘                               
par    └────────────┘ └──┘                               
pid    └─────────┘└─┘ └──┘                               
st   ─────────────────────────────────────────────────────────┘└─
187    { rw t_closure,
id          └───────┘
src      └─┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└──────────┘└─
188      assume y hy,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
189      by_cases h : y = a,
id                       
src      └───────┘ └─┘  
typ      └───────┘ └─┘ 
doc      └───────┘ └─┘  
txt      └───────┘ └─┘  
par      └───────┘ └─┘  
pid               └─┘  
st   ─────────────────────┘└─
190      { rw h, exact f_lim.mono ts },
id                    └────────┘ └┘
src        └─┘   └────┘└────────┘  
typ        └─┘  └────┘└────────┘└┘
doc        └─┘   └────┘            
txt        └─┘   └────┘            
par        └─┘   └────┘            
pid                              
st   ─────┘└──┘└────────────────────┘└┘
191      { have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩,
id                       └─┘        └────────────┘ └┘   
src        └─────┘   └──┘      └──┘└────────────┘  └─┘ 
typ        └─────┘ └──┘└─┘   └──┘└────────────┘└┘└─┘
doc        └─────┘   └──┘      └──┘                └─┘ 
txt        └─────┘   └──┘      └──┘                └─┘ 
par        └─────┘   └──┘      └──┘                └─┘ 
pid        └───┘└┘   └──┘      └──┘                └─┘ 
st   ──────────────────────────────────────────────────────┘└─
192        exact (f_diff.continuous_on y this).mono ts } },
id                └──────────────────┘  └──┘       └┘
src        └────┘ └──────────────────┘     └─────┘  
typ        └────┘ └──────────────────┘└──┘└─────┘└┘
doc        └────┘                          └─────┘  
txt        └────┘                          └─────┘  
par        └────┘                          └─────┘  
pid                                       └─────┘  
st   ─────────────────────────────────────────────────┘└──┘
193    have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)),
id                    └─────┘      └────┘        └─────────┘       └────────┘   
src    └─────────────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └────────┘└─┘ └┘
typ    └─────────────┘└─────┘  └─┘└────┘  └┘ └─────────┘└┘  └────────┘└─┘└┘
doc    └─────────────┘└─────┘  └─┘└────┘   └┘ └─────────┘  └┘  └────────┘└─┘ └┘
txt    └─────────────┘         └─┘         └┘              └┘             └─┘ └┘
par    └─────────────┘         └─┘         └┘              └┘             └─┘ └┘
pid    └──────────┘└─┘         └─┘         └┘              └┘             └─┘ └┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
194    { simp [deriv_fderiv.symm],
src      └────┘                 
typ      └────┘└───────────────┘
doc      └────┘                 
txt      └────┘                 
par      └────┘                 
pid                           
st   ───┘└──────────────────────┘└─
195      refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _,
id              └──────────┘ └───────────────────────────────────────────────────────────────┘
src      └─────┘└──────────┘└───────────────────────────────────────────────────────────────┘└┘
typ      └─────┘└──────────┘└───────────────────────────────────────────────────────────────┘└┘
doc      └─────┘            └───────────────────────────────────────────────────────────────┘└┘
txt      └─────┘                                                                             └┘
par      └─────┘                                                                             └┘
pid                                                                                         └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
196      exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' },
id             └─────────────┘  └──────────────┘   └─────────────────┘  └────┘
src      └────┘└─────────────┘ └──────────────┘└─┘└─────────────────┘└┘      
typ      └────┘└─────────────┘ └──────────────┘└─┘└─────────────────┘└┘└────┘
doc      └────┘                                └─┘                   └┘      
txt      └────┘                                └─┘                   └┘      
par      └────┘                                └─┘                   └┘      
pid                                           └─┘                   └┘      
st   ─────────────────────────────────────────────────────────────────────────┘└┘
197    -- now we can apply `has_fderiv_at_boundary_of_differentiable`
st   ─────────────────────────────────────────────────────────────────
198    have : has_deriv_within_at f e (Icc b a) a,
id            └─────────────────┘    └─┘     
src    └─────┘└─────────────────┘   └─┘  └┘
typ    └─────┘└─────────────────┘ └─┘ └┘
doc    └─────┘└─────────────────┘   └─┘  └┘
txt    └─────┘                           └┘
par    └─────┘                           └┘
pid    └───┘└┘                           └┘
st   ───────────────────────────────────────────┘└─
199    { rw [has_deriv_within_at_iff_has_fderiv_within_at, ← t_closure],
id           └──────────────────────────────────────────┘    └───────┘
src      └──┘└──────────────────────────────────────────┘└──┘         
typ      └──┘└──────────────────────────────────────────┘└──┘└───────┘
doc      └──┘└──────────────────────────────────────────┘└──┘         
txt      └──┘                                            └──┘         
par      └──┘                                            └──┘         
pid        └┘                                            └──┘         
st   ───┘└──────────────────────────────────────────────┘└───────────┘└──
200      exact has_fderiv_at_boundary_of_tendsto_fderiv t_diff t_conv t_open t_cont t_diff' },
id             └──────────────────────────────────────┘ └────┘ └────┘ └────┘ └────┘ └─────┘
src      └────┘└──────────────────────────────────────┘                               
typ      └────┘└──────────────────────────────────────┘└────┘└────┘└────┘└────┘└─────┘
doc      └────┘└──────────────────────────────────────┘                               
txt      └────┘                                                                       
par      └────┘                                                                       
pid                                                                                  
st   ──────────────────────────────────────────────────────────────────────────────────────┘└┘
201    exact this.nhds_within (mem_nhds_within_Iic_iff_exists_Icc_subset.2 ⟨b, ba, subset.refl _⟩)
id           └──────────────┘  └───────────────────────────────────────┘      └┘  └─────────┘
src    └────┘└──────────────┘ └───────────────────────────────────────┘└─┘  └┘  └┘└─────────┘└───┘
typ    └────┘└──────────────┘ └───────────────────────────────────────┘└─┘ └┘└┘└┘└─────────┘└───┘
doc    └────┘                 └───────────────────────────────────────┘└─┘  └┘  └┘           └───┘
txt    └────┘                                                          └─┘  └┘  └┘           └───┘
par    └────┘                                                          └─┘  └┘  └┘           └───┘
pid                                                                   └─┘  └┘  └┘           └──┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘
202  end
st   └─┘